$\exists$${\it code}$:$\mathbb{N}\rightarrow$(:$\mathbb{N}$ $\times$ $\mathbb{N}$). Surj($\mathbb{N}$;:$\mathbb{N}$ $\times$ $\mathbb{N}$;${\it code}$)